Program ::= '#' 'Variables'

                      Variables declare

                      '#' 'Initial'

                      Initial declare

                      '#' 'Protocol description'

                      Protocol declare

                      '#' 'System'

                      System declare

                      ('#' 'Intruder'

                      Intruder declare)?

                      ('#' 'Verification'

                      Verification declare)?

A.2 Declaration section

Variables declare  ::=  'Agents:'  List Id ';'

                                       ('Servers:'  List Id ';')?

                                       ('Nones:'  List Id ';')?

                                       ('Public keys:'  List Id ';')?

                                       ('Server keys:'  List Id ';')?

                                       ('Signature keys:'  List signaturekeys ';')?

                                       ('Inverse keys:'  List inversekeys ';')?

                                       ('Constants:'  List Id ';')?

                                       ('Functions:'  List Id ';')?

List Id    ::=  Id

                 |  Id, List Id

List serverkeys   ::=   '(' Id ','  Id ')'

                                  | '(' Id ','  Id ')'  ','  List serverkeys

List signaturekeys   ::=   '(' Id ','  Id ')'

                                        | '(' Id ','  Id ')'  ','  List signaturekeys

List inversekeys   ::=   '(' Id ','  Id ')'

                                    | '(' Id ','  Id ')'  ','  List inversekeys

A.3 Initial knowledge section

Initial declare  ::=  Id  'knows'   '{'   knowledge  '}'  ';'

                             | Id  'knows'   '{'   knowledge  '}'   ';'  Initial declare

knowledge     ::=   List Id

A.4 Protocol description section

Protocol declare   ::=   Id  '->' Id  ':'   message  ';'

                                     | Id  '->' Id  ':'   message   ';'  Protocol declare

message    ::=    msg  'Wait'  '['  number  ','   number  ']'

                          | msg  'timeout'   '['   number  ']'  msg

                          | msg   'interrupt'   '['   number   ']'   msg

                          | msg   'deadline'   '['   number   ']'

                          | msg

msg    ::=    msg1

                 | msg1   ','   msg

                 | '{'   msg   '}'   Id

                 | msg   '+'   msg

                 | Id   '('   msg   ')'                         //function declare

msg1   ::=   Id

                  | Id   ',' msg1

A.5 Actual system section

System declare   ::=    'Automatically'  ';'

                                    | 'Initiator'   ':'    List Id  ';'

                                      'Responder'   ':'   List Id  ';'

                                      ('Server'   ':'   List Id  ';')?

A.6 Intruder section

Intruder declare    ::=    'Intruder'   ':'   Id

                                        ('Intruder knowledge'   ':'   List Id)?

                                        ('Intruder ability'   ':'   List Id)?

A.7 Verification section

Verification declare    ::=    spec

                                           | temporal spec

                                           | spec,Verification declare

                                           | temporal spec,Verification declare

spec    ::=    ('Data secrecy:'   list secrecy   ';')?

                    ('Authentication:'   list auth   ';')?

                    ('Non repudiation:'    list condition   ';')?

                    ('Anonymity:'    list condition   ';')?

                    ('Fairness:'    list condition   ';')?

                    ('Integrity:'    Id   ';')?

list secrecy   ::=  Id 'of' Id

                          | Id 'of' Id   ','   list secrecy

list condition ::= Id 'condition is'   ':'   '{'   knowledge   '}'

                         | Id 'condition is'   ':'   '{'   knowledge   '}'   ','   list condition

list auth ::= Id 'is authenticated with' Id

                 | Id 'is authenticated with' Id   ','    list auth

temporal spec    ::=    'if'   temp formula   'then'   temp formula   ';'

temp formula ::= temp formula 'and' temp formula

                          | temp formula 'or' temp formula

                          | '(' temp formula ')'

                          | temp formula 'before' temp formula

                          | temp formula 'after' temp formula

                          | temp formula 'eventually' temp formula

                          | temp formula 'always' temp formula

                          | temp event

                          | '('  temp event  ')'  'within'   '['  number  ']'

temp event   ::=   Id  'sends'   message  ( 'to'  Id)?

                           | Id  'receives'  message (  'from'  Id)?

A.8 Basic definition

Identifier ::=  letter (letter | digit)*

letter        ::= 'a'..'z'  | 'A' .. 'Z' | '_'

digit ::= '0' .. '9'